Системы образующих и базисы. Теорема о существовании базиса.

Система векторов $\Sigma$ векторного пространства $V$ называется ***системой образующих*** этого пространства, если любой вектор из $V$ линейной выражается через какие-то вектора системы $\Sigma$

Если $\Sigma$ - система образующих векторного пространства $V$ и вектор $a \in \Sigma$ линейно выражается через другие вектора системы $\Sigma$, то и система $\Sigma/${$a$} является системой образующих в $V$

Покажем, что $\forall{x\in V}$ линейно выражается через какие-то вектора из $\Sigma/${$a$} $$x=\alpha_{1}a_{1}+\alpha_{2}a_{2}+\dots+\alpha_{n}a_{n}~~(*)$$ для некоторых $\alpha_{1},\alpha_{2},\dots,a_{n}\in F$ и $a_{1},a_{2},\dots,a_{n} \in \Sigma$. Если среди векторов $a_{1},a_{2},\dots,a_{n}$ нет $a$, то доказывать нечего. Если $a=a_{j}$ для некоторого $j$, подставим в $(*)$ вместо $a$ его выражение через другие вектора системы $\Sigma$ и получим выражение для $x$ через вектора из $\Sigma/${$a$} $~~~\square$

Базисом линейного пространства называется линейно независимая система образующих.

Если в ненулевом векторном пространстве $V$ есть конечная система образующих, то в $V$ есть и конечный базис.

Пусть $\Sigma$ - конечная система образующих пространства $V$. Если $\Sigma$ линейно независима, то доказывать нечего. Пусть $\Sigma$ линейно зависима. Удалив из $\Sigma$ нулевые вектора, получим систему образующих $\Sigma^`$. Пусть $\Sigma^`$ линейно зависима. По лемме о правом крайнем в $\Sigma^`$ есть вектор $a$, который линейно выражается через предыдущие. Тогда по лемме о прополке $\Sigma^`/${$a$} снова система образующих. Когда этот процесс остановится, получим базис.